T:Type, as, bs:T List, x:T.
((x  bs)  (agree_on_common(T;x.as;bs)  agree_on_common(T;as;bs)))
& ((x  as)  (agree_on_common(T;as;x.bs)  agree_on_common(T;as;bs))) 

latex

Definitions	t  T, x:A. B(x), agree_on_common(T;as;bs), P  Q, (x  l), A, P  Q, P & Q, ||as||, AB, , ij, False, True, P  Q, Prop, P  Q, {T}, SQType(T)
Lemmas	cons member, length cons, length wf2, agree on common nil, le wf, length wf1, length zero, non neg length, iff wf, agree on common wf, true wf, not wf, l member wf, ge wf, nat properties, nat wf